sum-deq(A;B;a;b)
== (A,B,a,b,p,q. Case q of
== (A,B,a,b,p,q. inl(x)  Case p of
== (A,B,a,b,p,q. inl(x)  inl(x1)  b/eq,b1.
== (A,B,a,b,p,q. inl(x)  inl(x1)  a/e1,a1.
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(%1.%1(x1,x)/%4,%5.
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(%4
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(((%1.%1)
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.((((%1.*)
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(((((%1.%1(x))
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.((((((%1.%1(x1))
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(((((((%1.%1(B))
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.((((((((%1.%1(A))
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.((((((((A,B,x1,x,%. (%1.%1)((%1.(%2.*)(*))(%))))))))))
== (A,B,a,b,p,q. inl(x)  inl(x1)  <%.(a1)
== (A,B,a,b,p,q. inl(x)  inl(x1)  ,%.*>
== (A,B,a,b,p,q. inl(x)  inr(y)  b/eq,b1.
== (A,B,a,b,p,q. inl(x)  inr(y)  a/e1,a1.
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(%1.any((%1(*))))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.((%1.%1(x))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((%1.%1(y))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.((((%1.%1(B))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((%1.%1(A))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.Case %1 of
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.inl(%2)  any(%2)
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.inr(%3)  (%4.any(%4))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.inr(%3)  ((%4.(%5.(%6.any(%6))(*))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.inr(%3)  ((%4.(*))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. (%1.inr(%3)  ((%)))
== (A,B,a,b,p,q. inl(x)  inr(y)  <%.(((((A,B,y,x,%. ((%1.%1)(inr(%.*))))))))
== (A,B,a,b,p,q. inl(x)  inr(y)  ,%.*>
== (A,B,a,b,p,q. inr(y)  Case p of
== (A,B,a,b,p,q. inr(y)  inl(x)  b/eq,b1.
== (A,B,a,b,p,q. inr(y)  inl(x)  a/e1,a1.
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(%1.any((%1(*))))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.((%1.%1(y))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((%1.%1(x))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.((((%1.%1(B))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((%1.%1(A))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.Case %1 of
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.inl(%2)  any(%2)
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.inr(%3)  (%4.any(%4))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.inr(%3)  ((%4.(%5.(%6.any(%6))(*))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.inr(%3)  ((%4.(*))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. (%1.inr(%3)  ((%)))
== (A,B,a,b,p,q. inr(y)  inl(x)  <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*))))))))
== (A,B,a,b,p,q. inr(y)  inl(x)  ,%.*>
== (A,B,a,b,p,q. inr(y)  inr(y1)  b/eq,b1.
== (A,B,a,b,p,q. inr(y)  inr(y1)  a/e1,a1.
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(%1.%1(y1,y)/%4,%5.
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(%4
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(((%1.%1)
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.((((%1.*)
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(((((%1.%1(y))
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.((((((%1.%1(y1))
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(((((((%1.%1(B))
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.((((((((%1.%1(A))
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.((((((((A,B,y1,y,%. (%1.%1)((%1.(%2.*)(*))(%))))))))))
== (A,B,a,b,p,q. inr(y)  inr(y1)  <%.(b1)
== (A,B,a,b,p,q. inr(y)  inr(y1)  ,%.*>)
== (A
== ,B
== ,a
== ,b) 

latex

Definitions	sum-deq(A;B;a;b)
FDL editor aliases	sum-deq